Goedel–McKinsey–Tarski translation